And in this case, that's very simple.

Instead of taking an actual closed term and substituting,

we'll just take a new variable.

Right? Looks like a term.

And I can later instantiate it with whatever I want.

This is singly branching.

Wonderful. I can just, boom, make progress.

Okay? And the thing gets smaller.

Wonderful. Ha!

Okay? There's a price to pray for at some point.

Remember our old rule saying, if I have A true and A false in the branch, I can close.

Well, at some point, I have to pay my debts.

I need a new rule.

Instead of saying if I have an A true and an A false in my proof, I can close directly,

but here I have to generalize this and say, oh, if I can make A and B equal by applying a substitution,

then I can close.

And if I do that, I apply the substitution to the whole tree, to the whole tableau.

Okay?

And that is wonderful.

That's a really, really, really big improvement because at this point,

it turns out that we can compute the substitutions that make these two equal,

and there's essentially a unique one.

And that algorithm is called unification, and it's an extremely important algorithm in computer science.

So back from this situation where we had no clue what to do and therefore had infinite branching,

we're moving the decision into the cut rule where we can compute the solution

by an algorithm called unification, which is very similar to what you did in high school

when you had these equation systems in arithmetics and kind of looked like this.

And you first forgot that, turned it into an upper triangle form, propagated, turned into this form,

and then it worked.

You remember that.

Essentially the same thing happens here.

Slightly different, even simpler.

Okay?

You can compute the solution, which means we've turned an infinitely branching search problem

into a computation problem, and that's a good thing.

And that's kind of an important idea, which turns the tableau calculus into something we can actually use.

Yeah, that should work.

There's another price to pay, and that's something called scolomization.

I'll play it safe.

Here, remember we had the rule where we just needed a single witness.

Now, if you look at this rule, what this amounts to is rename x by y and rip off the quantifier,

which means there's one more free variable in A, which you're later going to instantiate.

Now, here you can imagine that the witness you have to choose needs to be able to depend on your future choices,

which means that instead of having a single witness, you have a function that,

given any choice you're doing later, gives you a witness, and that's a so-called scolom function.

That's the other price you have to pay for this idea of delaying.

If you delay the choice of what you're talking about,

then you have to make sure that your witness can deal with whatever you can talk about.

And this is the technical trick, how we do that.

But these are the only tricks we have to do.